$\forall$${\it es}$:ES, $i$, $x$:Id, $T$, $A$:Type, $f$:($T$$\rightarrow$$A$).
\\[0ex]@$i$($x$:$T$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $f$(($x$ after $e$)) = $f$($x$ when $e$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $f$($x$ when $e$) = $f$($x$ when es{-}init(${\it es}$;$e$))